t:, w:World, ln:IdLnk. (0 < ||queue(ln;t)||)  (mlnk(hd(queue(ln;t))) = ln) 

latex

Definitions	x:A. B(x), P  Q, t  T, , (x  l), P  Q, Top, S  T, P & Q, P  Q, {i...j}, {i..j}, A  B, A, False, i  j < k, , x:A. B(x), A c B, Msg, i  j , l[i], nth_tl(n;as), Y, if b then t else f fi , i z j, b, i <z j, tt, ff, queue(l;t), snds(l;t), m(l;t), onlnk(l;mss)
Lemmas	length wf1, w-Msg wf, w-queue wf, IdLnk wf, world wf, nat wf, l member wf, general length nth tl, length wf nat, w-rcvs wf, top wf, w-action wf, ldst wf, w-snds wf, select nth tl, le wf, select wf, non neg length, member-concat, map wf, int seg wf, w-ml wf, upto wf, member map, member filter, eq lnk wf, w-m wf, lsrc wf, Msg wf, w-M wf, Id wf, mlnk wf, assert-eq-lnk, hd wf